$\forall$$T$:Type, $L$:($T$ List), $n$:int\_iseg(0; $\parallel$$L$$\parallel$). append(firstn($n$; $L$); nth\_tl($n$;$L$)) = $L$